f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
G2(s1(x), s1(y)) -> G2(x, y)
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
F3(t, x, y) -> G2(x, y)
f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
G2(s1(x), s1(y)) -> G2(x, y)
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
F3(t, x, y) -> G2(x, y)
f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
G2(s1(x), s1(y)) -> G2(x, y)
f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
G2(s1(x), s1(y)) -> G2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
G2(s1(x), s1(y)) -> G2(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
f3(t, x, y) -> f3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
F3(t, s1(x0), 0) -> F3(t, s1(x0), s1(0))
F3(t, s1(x0), s1(x1)) -> F3(g2(x0, x1), s1(x0), s1(s1(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(t, s1(x0), 0) -> F3(t, s1(x0), s1(0))
F3(t, s1(x0), s1(x1)) -> F3(g2(x0, x1), s1(x0), s1(s1(x1)))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
F3(t, s1(x0), s1(x1)) -> F3(g2(x0, x1), s1(x0), s1(s1(x1)))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
F3(t, s1(z0), s1(s1(z1))) -> F3(g2(z0, s1(z1)), s1(z0), s1(s1(s1(z1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
F3(t, s1(z0), s1(s1(z1))) -> F3(g2(z0, s1(z1)), s1(z0), s1(s1(s1(z1))))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)
f3(t, x0, x1)
f3(t, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
F3(t, x, y) -> F3(g2(x, y), x, s1(y))
g2(s1(x), 0) -> t
g2(s1(x), s1(y)) -> g2(x, y)
g2(s1(x0), s1(x1))
g2(s1(x0), 0)